p{-}mu($P$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $x$ of inl($n$) =$>$ ($\uparrow$($P$($n$))) \& ($\forall$$i$:\{0..$n$$^{-}$\}. $\neg$($\uparrow$($P$($i$)))) $\mid$ inr($z$) =$>$ $\forall$$i$:$\mathbb{N}$. $\neg$($\uparrow$($P$($i$)))